﻿using System;
using System.Collections.Generic;
using System.ComponentModel;
using System.Data;
using System.Drawing;
using System.Linq;
using System.Text;
using System.Windows.Forms;
using System.IO;
using Microsoft.FSharp.Core;
using System.Threading;

namespace CoreReset
{
    using ContextGraph = Dictionary<BIT_ARRAY.Bitarray, Dictionary<BIT_ARRAY.Bitarray, FSharpRef<BJK.sop_bar.DFR>>>;
    using Microsoft.Glee.Drawing;
    
    /// <summary>
    /// This delgate is used in order to invoke the setResultText method
    /// from a different thread (the analysis thread).
    /// </summary>
    /// <param name="text">The result text.</param>
    /// <param name="g">The computed context graph.</param>
    delegate void SetResultTextCallback(string text, ContextGraph g);
    
    /// <summary>
    /// This delgate is used in order to invoke the setAnalyseButtonImage method
    /// from a different thread (the analysis thread).
    /// </summary>
    /// <param name="cancel">If true, the Analyse button is changed to a "cancel" button.</param>
    delegate void SetAnalyseButtonImageCallback(bool cancel);
    
    /// <summary>
    /// This delgate is used in order to invoke the ClearLastHighlightedCommand method
    /// from a different thread (the analysis thread).
    /// </summary>
    delegate void ClearLastHighlightedCommandCallback();
    
    /// <summary>
    /// This delgate is used in order to invoke the UpdateCommandGraph method
    /// from a different thread (the analysis thread).
    /// </summary>
    /// <param name="args">Command Graph arguments - containing a command and its associated context graph.</param>
    delegate void UpdateProgramTreeCallback(FSEvent.CommandGraphUpdatedEventArgs args);

    /// <summary>
    /// This is the main application form.
    /// </summary>
    public partial class CoreResetForm : Form
    {
        /// <summary>
        /// A command tree node is a TreeNode which holds
        /// properties associated with a core language command:
        /// Context Graph(as data structure and as textual string) and Id. 
        /// </summary>
        public class CmdTreeNode : TreeNode
        {
            /// <summary>
            /// Constructor.
            /// </summary>
            /// <param name="id">The command identifier.</param>
            /// <param name="text">The command text (the text appearing in the AST).</param>
            public CmdTreeNode(int id, string text)
                : base(text)
            {
                m_id = id;
            }

            /// <summary>
            /// Gets the command identifier.
            /// </summary>
            public int Id
            {
                get
                {
                    return m_id;
                }
            }

            /// <summary>
            /// Gets or sets the context graph associated with the command.
            /// </summary>
            public ContextGraph Graph
            {
                get
                {
                    return m_graph;
                }
                set
                {
                    m_graph = value;
                }
            }

            /// <summary>
            /// Gets or sets the context graph (in textual format) associated with the command.
            /// </summary>
            public string GraphText
            {
                get
                {
                    return m_GraphText;
                }
                set
                {
                    m_GraphText = value;
                }
            }

            /// <summary>
            /// The command identifier.
            /// </summary>
            int m_id = -1;

            /// <summary>
            /// The command's associated context graph in textual format.
            /// </summary>
            private string m_GraphText = null;

            /// <summary>
            /// The command's associated context graph as data-structure.
            /// </summary>
            private ContextGraph m_graph = null;
        }

        /// <summary>
        /// The AST tree node which was last highlighted.
        /// </summary>
        TreeNode m_lastHighlightedNode = null;

        /// <summary>
        /// The analysis thread continues as long as this flag is true.
        /// </summary>
        volatile bool m_shouldContinue = false;

        /// <summary>
        /// When true, analysis will be executed step-by-step.
        /// </summary>
        volatile bool m_stepByStep = false;

        /// <summary>
        /// Placeholder for the analysis thread.
        /// </summary>
        private volatile Thread m_analysisThread = null;

        /// <summary>
        /// Placeholder for the "Analyse" button tool-tip.
        /// </summary>
        private ToolTip m_analyseToolTip = null;

        /// <summary>
        /// Placeholder for other button tool-tips.
        /// </summary>
        private ToolTip m_generalToolTip = null;

        /// <summary>
        /// Reference to the debug log form.
        /// </summary>
        private volatile DebugLogForm m_debugLogForm = null;

        /// <summary>
        /// Reference to the Command Graph form.
        /// </summary>
        private CommandGraphForm m_commandGraphForm = null;

        /// <summary>
        /// When true, the analysis thread dumps debug information using a
        /// specialized event.
        /// </summary>
        private volatile bool m_registeredToDebugEvent = false;

        /// <summary>
        /// Reference to the last computed AST.
        /// </summary>
        private CoreEx.Cmd m_lastAST = null;

        /// <summary>
        /// When true, original variable names are shown in the AST, otherwise
        /// the variables shown will be X1,X2,...,Xn (a mapping between original variables
        /// and the Xi's is shown in the Analysis Results window).
        /// </summary>
        private bool m_showOriginalVarNamesInAST = false;

        /// <summary>
        /// The current abstract interpreter algorithm object.
        /// </summary>
        ABSTRACT_INTERPRETER.AbstractInterpreter m_absInt;
        
        /// <summary>
        /// A Polynomial/Non-Polynomial classification abstract interpreter algorithm object.
        /// </summary>
        ABSTRACT_INTERPRETER.AbstractInterpreter m_polyAbsInt = ABSTRACT_INTERPRETER.Poly;

        /// <summary>
        /// A Linear/Non-Linear classification abstract interpreter algorithm object.
        /// </summary>
        ABSTRACT_INTERPRETER.AbstractInterpreter m_linAbsInt = ABSTRACT_INTERPRETER.Lin;

        /// <summary>
        /// The current naive algorithm object.
        /// </summary>
        NAIVE_ANALYSIS.NaiveAnalysis m_naiveAnalysis;
        /// <summary>
        /// Polinomial Complexity Analysis algorithm object.
        /// </summary>
        POLY_COMP_ANALYSIS.PolyCompAnalysis m_PolyCompAnalysis = POLY_COMP_ANALYSIS.Poly;
        /// <summary>
        /// A Polynomial/Non-Polynomial classification naive algorithm object.
        /// </summary>
        NAIVE_ANALYSIS.NaiveAnalysis m_polyNaiveAnalysis = NAIVE_ANALYSIS.Poly;

        /// <summary>
        /// A Linear/Non-Linear classification naive algorithm object.
        /// </summary>
        NAIVE_ANALYSIS.NaiveAnalysis m_linNaiveAnalysis = NAIVE_ANALYSIS.Lin;

        /// <summary>
        /// This flag is set to true during closing of this form.
        /// </summary>
        private bool m_formClosing = false;

        /// <summary>
        /// Window title excluding current file name and dirty flag.
        /// </summary>
        private string baseTitle;
        
        /// <summary>
        /// Last saved code text, for dirty flag computation.
        /// </summary>
        private string baseCodeValue;
        
        /// <summary>
        /// Current file name loaded, or null if none.
        /// </summary>
        private string currentFileName = null;

        /// <summary>
        /// Constructor.
        /// </summary>
        public CoreResetForm()
        {
            InitializeComponent();
            comboBoxAlgoSelect.SelectedIndex = 3;
            comboBoxAnalysisType.SelectedIndex = 2;
            m_analyseToolTip = new ToolTip();
            m_analyseToolTip.SetToolTip(buttonAnalyse, "Analyse program");
            m_generalToolTip = new ToolTip();
            m_generalToolTip.SetToolTip(buttonOpenCodeFile, "Open Core Language program file");
            m_generalToolTip.SetToolTip(buttonContinue, "Analyse program step-by-step");
            m_generalToolTip.SetToolTip(buttonShowDebugLog, "Show analysis log");

            MRU.UpdateMRUMenu(recentFilesToolStripMenuItem);
            MRU.ItemClicked += new MRUEventHandler(MRU_ItemClicked);
            baseTitle = this.Text;
            baseCodeValue = CodeTextBox.Text;
            UpdateTitle();
        }

        /// <summary>
        /// Updates the analysis final results to the Analysis Results pane and
        /// updated the Command Graph Form with the last computed graph.
        /// </summary>
        /// <param name="s">Context graph in textual format.</param>
        /// <param name="g">Context graph.</param>
        private void setResultText(string s, ContextGraph g)
        {
            textBoxAnalysisResult.Lines = s.Split('\n');
            if (m_commandGraphForm != null && !m_stepByStep && ASTreeView.Nodes != null && ASTreeView.Nodes.Count > 0)
            {
                CmdTreeNode node = ASTreeView.Nodes[0].Nodes[0] as CmdTreeNode;
                if (node != null && g != null)
                {
                    node.GraphText = s;
                    node.Graph = CG.clone(g);
                    ASTreeView.Select();
                    ASTreeView.SelectedNode = node;
                    ShowCommandGraph(node, true);
                }
            }
        }

        /// <summary>
        /// Retrieves the text displayed in the AST for a command by its identifier.
        /// </summary>
        /// <param name="id">The command identifier.</param>
        /// <returns>the text displayed in the AST for the command.</returns>
        public string GetCommandText(int id)
        {
            string txt = "";
            CmdTreeNode node = GetTreeNodeById(ASTreeView.TopNode, id) as CmdTreeNode;
            if (node != null)
                txt = node.Text;
            return txt;
        }

        /// <summary>
        /// Given a command identifier, returns the number of commands on its premises
        /// (0, 1 or 2).
        /// </summary>
        /// <param name="id">The command identifier.</param>
        /// <returns>The number of commands on the command premises.</returns>
        public int ChildNumberUnderBranch(int id)
        {
            int rc = 0;
            CmdTreeNode node = GetTreeNodeById(ASTreeView.TopNode, id) as CmdTreeNode;
            if (node != null)
            {
                CmdTreeNode parent = node.Parent as CmdTreeNode;
                if (parent != null && parent.Text.StartsWith("Choose")) 
                {
                    if (parent.Nodes[0] == node)
                        rc = 1;
                    else
                        rc = 2;
                }
            }

            return rc;
        }

        /// <summary>
        /// Extracts a CmdEx command from a CoreEx.Cmd.
        /// This can either be a Naive analysis algorithm command or
        /// an abstract interpreter algorithim command (associated with
        /// a context graph).
        /// </summary>
        private CoreEx.CmdEx GetCmdEx(CoreEx.Cmd cmd)
        {
            if (cmd.IsAICmd)
            {
                return (cmd as CoreEx.Cmd.AICmd).Item1;
            }
            else if (cmd.IsNaiveCmd)
            {
                return (cmd as CoreEx.Cmd.NaiveCmd).Item1;
            }
            else if (cmd.IsPolyCompCmd)
            {
                return (cmd as CoreEx.Cmd.PolyCompCmd).Item1;
            }

            return null;
        }

        /// <summary>
        /// Returns a command identifier as string.
        /// </summary>
        private string cmdIdStr(CoreEx.Cmd cmd)
        {
            if (cmd.IsAICmd)
            {
                return (cmd as CoreEx.Cmd.AICmd).Item3.ToString();
            }
            else if (cmd.IsNaiveCmd)
            {
                return (cmd as CoreEx.Cmd.NaiveCmd).Item2.ToString();
            }
            else if (cmd.IsPolyCompCmd)
            {
                return (cmd as CoreEx.Cmd.PolyCompCmd).Item2.ToString();
            }

            return (-1).ToString();
        }

        /// <summary>
        /// Returns a command identifier as integer.
        /// </summary>
        private int cmdId(CoreEx.Cmd cmd)
        {
            if (cmd.IsAICmd)
            {
                return (cmd as CoreEx.Cmd.AICmd).Item3;
            }
            else if (cmd.IsNaiveCmd)
            {
                return (cmd as CoreEx.Cmd.NaiveCmd).Item2;
            }
            else if (cmd.IsPolyCompCmd)
            {
                return (cmd as CoreEx.Cmd.PolyCompCmd).Item2;
            }

            return -1;
        }

        /// <summary>
        /// Adds an AST node for the given command.
        /// </summary>
        /// <param name="parent">The new AST node is added as a child of 'parent'.</param>
        /// <param name="cmd">The command for which the new AST node is created.</param>
        private void addASTNode(CmdTreeNode parent, CoreEx.Cmd cmd)
        {
            CmdTreeNode child = null;
            CoreEx.CmdEx c = GetCmdEx(cmd);
            if (c.IsChoice)
            {
                child = new CmdTreeNode(cmdId(cmd),"Choose / or (" + cmdId(cmd) + ")");
                CoreEx.CmdEx.Choice choice = c as CoreEx.CmdEx.Choice;
                addASTNode(child, choice.Item1);
                addASTNode(child, choice.Item2);
            }
            else if (c.IsLoop)
            {
                CoreEx.CmdEx.Loop loop = c as CoreEx.CmdEx.Loop;
                child = new CmdTreeNode(cmdId(cmd), "Loop " + getVarNameByVarIndex(loop.Item1) + " (" + cmdId(cmd) + ")");
                addASTNode(child, loop.Item2);
            }
            else if (c.IsSeq)
            {
                child = new CmdTreeNode(cmdId(cmd), "Sequence" + " (" + cmdId(cmd) + ")");
                CoreEx.CmdEx.Seq seq = c as CoreEx.CmdEx.Seq;
                addASTNode(child, seq.Item1);
                addASTNode(child, seq.Item2);
            }
            else if (c.IsSkip)
            {
                child = new CmdTreeNode(cmdId(cmd), "Skip" + " (" + cmdId(cmd) + ")");
            }
            else if (c.IsAsgn)
            {
                CoreEx.CmdEx.Asgn asgn = c as CoreEx.CmdEx.Asgn;
                string expr = exprString(asgn.Item2);
                int varIndex = asgn.Item1;
                string varName = getVarNameByVarIndex(varIndex);
                child = new CmdTreeNode(cmdId(cmd), varName + " := " + expr + " (" + cmdId(cmd) + ")");
            }
            

            parent.Nodes.Add(child);
        }

        /// <summary>
        /// Retrieves the variable name by its index.
        /// Will work only after an analysis was executed.
        /// </summary>
        /// <param name="varIndex"></param>
        /// <returns></returns>
        private string getVarNameByVarIndex(int varIndex)
        {
            string varStr = "X" + varIndex.ToString();
            if (m_showOriginalVarNamesInAST && BJKParse.parserLastVarToIndexMap().ContainsKey(varIndex))
            {
                varStr = BJKParse.parserLastVarToIndexMap()[varIndex];
            }
            return varStr; 
        }

        /// <summary>
        /// Converts a core language expression to string.
        /// </summary>
        private string exprString(Core.Expr expr)
        {
            string res = null;
            if (expr.IsPlus)
            {
                 Core.Expr.Plus plus = expr as Core.Expr.Plus;
                 res = exprString(plus.Item1) + " + " + exprString(plus.Item2);
            }
            else if (expr.IsTimes)
            {
                Core.Expr.Times times = expr as Core.Expr.Times;
                res = exprString(times.Item1) + " * " + exprString(times.Item2);
            }
            else if (expr.IsVar)
            {
                Core.Expr.Var v = expr as Core.Expr.Var;
                res = getVarNameByVarIndex(v.Item);
            }
            else if (expr.IsZero)
            {
                res = "0";
            }
            return res;
        }

        /// <summary>
        /// Updates the AST pane to display the given command's AST.
        /// </summary>
        /// <param name="ast">The AST root command.</param>
        private void updateAST(CoreEx.Cmd ast)
        {
            ASTreeView.Nodes.Clear();
            ASTreeView.Nodes.Add(new CmdTreeNode(-1,"Program"));
            addASTNode(ASTreeView.TopNode as CmdTreeNode, ast);
            ASTreeView.ExpandAll();
        }

        /// <summary>
        /// Enumeration which defines the possible analysis classification types
        /// </summary>
        enum AnalysisType
        {
            Poly, //Polynomial/Non-polynomial classification
            Lin   //Linear/Non-linear classification
        }

        /// <summary>
        /// Enumeration which defines the availabe analysis algorithms
        /// </summary>
        enum AlgoType
        {
            BJK,
            Naive,
            AbsInt,
            PolyComp
        }

        private void setResultTextSafe(string text,ContextGraph g)
        {
            if (this.textBoxAnalysisResult.InvokeRequired)
            {
                SetResultTextCallback d = new SetResultTextCallback(setResultText);
                this.Invoke(d, new object[] { text,g });
            }
            else
            {
                setResultText(text,g);
            }
        }

        private void setAnalyseButtonImageSafe(bool cancel)
        {
            if (this.buttonAnalyse.InvokeRequired)
            {
                SetAnalyseButtonImageCallback d = new SetAnalyseButtonImageCallback(setAnalyseButtonImage);
                this.Invoke(d, new object[] { cancel });
            }
            else
            {
                setAnalyseButtonImage(cancel);
            }
        }

        private void clearLastHighlightedCommandSafe()
        {
            if (this.ASTreeView.InvokeRequired)
            {
                ClearLastHighlightedCommandCallback d = new ClearLastHighlightedCommandCallback(ClearLastHighlightedCommand);
                this.Invoke(d, new object[] { });
            }
            else
            {
                ClearLastHighlightedCommand();
            }
        }

        private struct AnalysisThreadParams
        {
            public AnalysisThreadParams(Core.Cmd c_, AnalysisType t_, AlgoType a_)
            {
                c = c_;
                type = t_;
                algo = a_;
            }
            public Core.Cmd c;
            public AnalysisType type;
            public AlgoType algo;
        }

        private void setAnalyseButtonImage(bool cancel)
        {
            m_analyseToolTip.RemoveAll();
            if (cancel)
            {
                m_analyseToolTip.SetToolTip(buttonAnalyse, "Analysis In Progress...\nClick to abort.");
                buttonAnalyse.Image = Properties.Resources.Cancel_icon;
            }
            else
            {
                m_analyseToolTip.SetToolTip(buttonAnalyse, "Analyse Program");
                buttonAnalyse.Image = Properties.Resources.Icon_Gear02_Blue;
            }
        }
         
        private TreeNode GetTreeNodeById(TreeNode root, int id)
        {
            CmdTreeNode node = root as CmdTreeNode;
            if (node != null )
            {
                if (node.Id == id)
                {
                    return root;
                }
                else 
                {
                    foreach (TreeNode child in root.Nodes)
                    {
                        TreeNode found = GetTreeNodeById(child, id);
                        if (found != null)
                            return found;
                    }
                }
            }
            return null;
        }

        private void safeUpdateCommandGraph(FSEvent.CommandGraphUpdatedEventArgs args)
        {
            if (this.ASTreeView.InvokeRequired)
            {
                UpdateProgramTreeCallback d = new UpdateProgramTreeCallback(UpdateCommandGraph);
                this.Invoke(d, new object[] { args });
            }
            else
            {
                UpdateCommandGraph(args);
            }

        }

        private void UpdateCommandGraph(FSEvent.CommandGraphUpdatedEventArgs args)
        {
            int id = cmdId(args.Command);
            ClearLastHighlightedCommand();
            CmdTreeNode cmdNode = GetTreeNodeById(ASTreeView.TopNode, id) as CmdTreeNode;
            if (cmdNode != null)
            {
                cmdNode.GraphText = "";
                HighlightCommand(cmdNode);
                if (args.GraphExist)
                {
                    cmdNode.GraphText += CG.prtEdges(args.Graph);
                    cmdNode.Graph = CG.clone(args.Graph);
                }
                if (args.CmdTextExist)
                    cmdNode.GraphText += args.CmdText;

                ShowCommandGraph(cmdNode, false);

            }
        }


        private void HighlightCommand(CmdTreeNode cmdNode)
        {
            cmdNode.BackColor = System.Drawing.Color.Blue;
            cmdNode.ForeColor = System.Drawing.Color.Yellow;
            m_lastHighlightedNode = cmdNode;
        }

        private void ClearLastHighlightedCommand()
        {
            if (m_lastHighlightedNode != null)
            {
                m_lastHighlightedNode.BackColor = System.Drawing.Color.White;
                m_lastHighlightedNode.ForeColor = System.Drawing.Color.Black;
            }
        }
        private void ThreadedAnalysisFunc(object obj)
        {
            try
            {
                ContextGraph g = null;
                AnalysisThreadParams p = (AnalysisThreadParams)obj;
                Core.Cmd ast = p.c;

                string resText = null;

                Int32 startTime = 0;

                if (!m_stepByStep)
                {
                    startTime = System.Environment.TickCount;
                }
                bool polyAnalysis = (p.type == AnalysisType.Poly);
                string edgeCount = "";
                if (p.algo == AlgoType.BJK)
                {
                    //BJK algorithm
                    BJK.Analysis.analysis analysis = polyAnalysis ? BJK.Analysis.Pol : BJK.Analysis.Lin;
                    BJK.sop_bar.DFR dfr = analysis.analyse(ast);
                    
                    Microsoft.FSharp.Collections.FSharpList<CG.edge> edgeList = Microsoft.FSharp.Collections.FSharpList<CG.edge>.Empty; 
                    BIT_ARRAY.Bitarray emptyContext = BIT_ARRAY.BitarrayModule.create(1);
                    g = CG.newGraph(edgeList);
                    CG.edge e = CG.edge.NewE(emptyContext,emptyContext,new FSharpRef<BJK.sop_bar.DFR>(dfr));
                    CG.addEdge(g, e, false);                    
                    resText = analysis.resultText(ast, dfr);
                }
                else if (p.algo == AlgoType.Naive)
                {
                    m_naiveAnalysis = polyAnalysis ? NAIVE_ANALYSIS.Poly : NAIVE_ANALYSIS.Lin;
                    RegisterAnalysisEvents();
                    g = m_naiveAnalysis.analyse(ast);
                    edgeCount = "\nContext graph contains " + CG.untaggedEdges(g).Length.ToString() + " edges.";
                    UnregisterAnalysisEvents();
                    resText = "Variable indices:\n" + BJKParse.parserLastVarMapping() + "\nContext Graph:\n" + CG.prtEdges(g) + m_naiveAnalysis.resultText(ast, g);
                }
                else if (p.algo == AlgoType.PolyComp)
                {         
                    // Run BJK algorithm to get non polynomial variables
                    BJK.Analysis.analysis analysis = BJK.Analysis.Pol;
                    BJK.sop_bar.DFR dfr = analysis.analyse(ast);

                    Microsoft.FSharp.Collections.FSharpList<CG.edge> edgeList = Microsoft.FSharp.Collections.FSharpList<CG.edge>.Empty;
                    Microsoft.FSharp.Collections.FSharpList<int> nonboundedList = analysis.nonboundedList(ast, dfr);

                    // run PolyComp
                    m_PolyCompAnalysis = POLY_COMP_ANALYSIS.Poly;
                    RegisterAnalysisEvents();
                    m_PolyCompAnalysis.analyse(ast);
                    UnregisterAnalysisEvents();
                    resText = m_PolyCompAnalysis.GetResult(nonboundedList);
                    g = null;
                }
                else //abstract interpreter
                {
                    m_absInt = polyAnalysis ? ABSTRACT_INTERPRETER.Poly : ABSTRACT_INTERPRETER.Lin;
                    RegisterAnalysisEvents();
                    g = m_absInt.analyse(ast);
                    edgeCount = "\nContext graph contains " + CG.untaggedEdges(g).Length.ToString() + " edges.";
                    UnregisterAnalysisEvents();
                    resText = "Variable indices:\n" + BJKParse.parserLastVarMapping() + "\nContext Graph:\n" + CG.prtEdges(g) + m_absInt.resultText(ast, g);
                }
                m_stepByStep = false;
                Int32 elapsedTime = System.Environment.TickCount - startTime;
                double dElapsedTime = ((double)elapsedTime) / 1000.0;
                if (startTime != 0)
                {
                    resText = "Analysis complete in " + dElapsedTime.ToString() + " seconds." + edgeCount + "\n\n" + resText;
                }
                setResultTextSafe(resText,g);
            }
            catch (Util.Fail f)
            {
                MessageBox.Show(f.Data0, "Error", MessageBoxButtons.OK, MessageBoxIcon.Error);
                setResultTextSafe("Analysis failed.",null);
            }
            finally
            {
                m_analysisThread = null;
                if (!m_formClosing)
                {
                    setAnalyseButtonImageSafe(false);
                    clearLastHighlightedCommandSafe();
                }
            }
        }

        private void UnregisterAnalysisEvents()
        {
            if (m_stepByStep)
            {
                m_polyAbsInt.CommandGraphUpdated -= new Microsoft.FSharp.Control.FSharpHandler<FSEvent.CommandGraphUpdatedEventArgs>(ai_CommandGraphUpdated);
//                m_linAbsInt.CommandGraphUpdated -= new Microsoft.FSharp.Control.FSharpHandler<ABSTRACT_INTERPRETER.CommandGraphUpdatedEventArgs>(ai_CommandGraphUpdated);
            }
            //m_polyAbsInt.DebugInfoAdded -=
            //  new Microsoft.FSharp.Control.FSharpHandler<ABSTRACT_INTERPRETER.DebugInfoAddedEventArgs>(OnDebugInfoAdded);
            //m_linAbsInt.DebugInfoAdded -=
            //  new Microsoft.FSharp.Control.FSharpHandler<ABSTRACT_INTERPRETER.DebugInfoAddedEventArgs>(OnDebugInfoAdded);
        }

        private void RegisterAnalysisEvents()
        {
            if (m_stepByStep)
            {
                m_polyAbsInt.CommandGraphUpdated += new Microsoft.FSharp.Control.FSharpHandler<FSEvent.CommandGraphUpdatedEventArgs>(ai_CommandGraphUpdated);
 //               m_linAbsInt.CommandGraphUpdated += new Microsoft.FSharp.Control.FSharpHandler<ABSTRACT_INTERPRETER.CommandGraphUpdatedEventArgs>(ai_CommandGraphUpdated);
            }
            if (!m_registeredToDebugEvent)
            {
                m_registeredToDebugEvent = true;
                m_polyAbsInt.DebugInfoAdded +=
                    new Microsoft.FSharp.Control.FSharpHandler<FSEvent.DebugInfoAddedEventArgs>(OnDebugInfoAdded);
                m_PolyCompAnalysis.DebugInfoAdded +=
                    new Microsoft.FSharp.Control.FSharpHandler<FSEvent.DebugInfoAddedEventArgs>(OnDebugInfoAdded);
            }
        }

        void ai_CommandGraphUpdated(object sender, EventArgs e)
        {
            FSEvent.CommandGraphUpdatedEventArgs cmdArgs = e as FSEvent.CommandGraphUpdatedEventArgs;
            if (cmdArgs != null)
                safeUpdateCommandGraph(cmdArgs);
            while (!m_shouldContinue)
            {
                Thread.Sleep(10);
            }
            m_shouldContinue = false;

        }

        private void Analyze(bool inSteps)
        {
            try
            {
                m_shouldContinue = false;
                m_stepByStep = inSteps;
                Core.Cmd c = BJKParse.astBreakNestedExpressions(BJKParse.aString(CodeTextBox.Text));

                AlgoType at = getAlgoType();
                switch (at)
                {
                    default:
                    case AlgoType.AbsInt    : m_lastAST = CoreEx.extendedAbsIntAST(c);      break;
                    case AlgoType.BJK       : m_lastAST = CoreEx.extendedNaiveAST(c);       break;
                    case AlgoType.PolyComp  : m_lastAST = CoreEx.extendedPolyCompAST(c);    break;
                }

                updateAST(m_lastAST);
                if (m_debugLogForm != null)
                    m_debugLogForm.ClearText();
                setAnalyseButtonImageSafe(true);
                m_analysisThread = new Thread(new ParameterizedThreadStart(ThreadedAnalysisFunc));
                textBoxAnalysisResult.Clear();
                textBoxAnalysisResult.Text = "Analysing...";
                m_analysisThread.Start(new AnalysisThreadParams(c, getAnalysisType(), getAlgoType()));  
            }
            catch (Util.Fail f)
            {
                MessageBox.Show(f.Data0, "Error", MessageBoxButtons.OK, MessageBoxIcon.Error);
                m_analysisThread = null;
                setAnalyseButtonImageSafe(false);
            }
        }

        private void buttonAnalyse_Click(object sender, EventArgs e)
        {
            if (m_analysisThread != null)
            {
                //analysis is running - abort it.
                AbortAnalysis();
            }
            else
            {
                Analyze(false);
            }
        }

        private void AbortAnalysis()
        {
            if (m_analysisThread != null)
            {
                m_analysisThread.Abort();
                m_analysisThread = null;
                if (!m_formClosing)
                {
                    setAnalyseButtonImageSafe(false);
                    UnregisterAnalysisEvents();
                    textBoxAnalysisResult.Clear();
                    textBoxAnalysisResult.Text = "Analysis aborted.";

                    m_stepByStep = false;
                }
            }
         }

        private AlgoType getAlgoType()
        {
            AlgoType at = AlgoType.AbsInt;
            if (comboBoxAlgoSelect.SelectedIndex == 0)
                at = AlgoType.BJK;
            else if (comboBoxAlgoSelect.SelectedIndex == 1)
                at = AlgoType.Naive;
            else if (comboBoxAlgoSelect.SelectedIndex == 3)
                at = AlgoType.PolyComp;
            return at;
        }

        private AnalysisType getAnalysisType()
        {
            AnalysisType at = AnalysisType.Lin;
            if (comboBoxAnalysisType.SelectedIndex == 0)
                at = AnalysisType.Poly;
            return at;
        }

        private void CoreResetForm_FormClosing(object sender, FormClosingEventArgs e)
        {
            // File management - prompt user to save changes before quitting.
            bool cancel = CheckUnsavedChanges();
            if (cancel)
            {
                e.Cancel = cancel;
                return;
            }

            m_formClosing = true;
            AbortAnalysis();
            if (m_commandGraphForm != null)
            {
                m_commandGraphForm.Close();
            }
            if (m_debugLogForm != null)
            {
                m_debugLogForm.Close();
            }
        }

        private void buttonAbout_Click(object sender, EventArgs e)
        {
            AboutForm frm = new AboutForm();
            frm.ShowDialog();
        }

        private void buttonContinue_Click(object sender, EventArgs e)
        {
            if (!m_stepByStep)
            {
                m_stepByStep = true;
                Analyze(true);
            }
            else
            {
                m_shouldContinue = true;
            }
        }

        private void buttonShowDebugLog_Click(object sender, EventArgs e)
        {
            m_polyAbsInt.setDebugMode(true);
            m_linAbsInt.setDebugMode(true);
            m_PolyCompAnalysis.setDebugMode(true);
            if (m_debugLogForm == null)
            {
                m_debugLogForm = new DebugLogForm(this);
            }
            if (!m_debugLogForm.Visible)
            {
                m_debugLogForm.Show(this);
                buttonShowDebugLog.Enabled = false;
            }
            if (m_absInt != null && !m_registeredToDebugEvent)
            {
                m_registeredToDebugEvent = true;
                m_polyAbsInt.DebugInfoAdded += 
                    new Microsoft.FSharp.Control.FSharpHandler<FSEvent.DebugInfoAddedEventArgs>(OnDebugInfoAdded);
            }

        }

        internal void OnDebugLogFormClosing()
        {
            if (m_absInt != null)
            {
                ABSTRACT_INTERPRETER.Poly.setDebugMode(false);
                ABSTRACT_INTERPRETER.Lin.setDebugMode(false);
                if (m_registeredToDebugEvent)
                {
                    m_polyAbsInt.DebugInfoAdded -=
                        new Microsoft.FSharp.Control.FSharpHandler<FSEvent.DebugInfoAddedEventArgs>(OnDebugInfoAdded);
                    m_registeredToDebugEvent = false;
                }
            }
            buttonShowDebugLog.Enabled = true;
        }

        private void OnDebugInfoAdded(object sender, EventArgs args)
        {
            FSEvent.DebugInfoAddedEventArgs eArgs = args as FSEvent.DebugInfoAddedEventArgs;
            if (eArgs != null && m_debugLogForm != null)
            {
                m_debugLogForm.AddText(eArgs.Text);
            }
        }

        internal void OnCommandGraphFormClosing()
        {
            m_commandGraphForm = null;
        }

        private void ASTreeView_NodeMouseClick(object sender, TreeNodeMouseClickEventArgs e)
        {
            CmdTreeNode cmdNode = e.Node as CmdTreeNode;
            ShowCommandGraph(cmdNode, true);
        }

        private void ShowCommandGraph(CmdTreeNode cmdNode, bool forceOpen)
        {
            if (cmdNode != null && cmdNode.GraphText != null)
            {
                if (m_commandGraphForm == null)
                {
                    m_commandGraphForm = new CommandGraphForm(this, cmdNode.GraphText);
                }
                else
                {
                    m_commandGraphForm.SetText(cmdNode.GraphText);
                    if (cmdNode.Graph != null)
                        m_commandGraphForm.SetGraph(cmdNode.Graph);
                }
                if (!m_commandGraphForm.Visible && forceOpen)
                {
                    m_commandGraphForm.Show(this);
                }
            }
            else if (m_commandGraphForm != null)
            {
                m_commandGraphForm.SetText("");
            }
            else
            {
                m_commandGraphForm = new CommandGraphForm(this, "");
                m_commandGraphForm.Show(this);
            }
        }

        private void comboBoxAlgoSelect_SelectedIndexChanged(object sender, EventArgs e)
        {
            bool shouldEnableStepByStep = comboBoxAlgoSelect.SelectedIndex > 0;
            buttonContinue.Enabled = shouldEnableStepByStep;

            if (comboBoxAlgoSelect.SelectedIndex == 3)
                comboBoxAnalysisType.SelectedIndex = 2;
            else if (comboBoxAnalysisType.SelectedIndex == 2)
                comboBoxAnalysisType.SelectedIndex = 0;
        }

        private void checkBoxShowOriginalVarNames_CheckedChanged(object sender, EventArgs e)
        {
            m_showOriginalVarNamesInAST = checkBoxShowOriginalVarNames.Checked;
            if (ASTreeView.Nodes.Count > 0 && m_lastAST != null)
            {
                updateAST(m_lastAST);
            }
        }      

        // Menu and files management

        /// <summary>
        /// Event procedure when clicking on an MRU entry from the 'Recent Files' menu.
        /// </summary>
        void MRU_ItemClicked(object sender, MRUEventArgs e)
        {
            if (CheckUnsavedChanges()) return;
            try
            {
                var text = File.ReadAllText(e.FileName);
                CodeTextBox.Text = text;
                MRU.Insert(e.FileName);
                MRU.UpdateMRUMenu(recentFilesToolStripMenuItem);
                currentFileName = e.FileName;
                baseCodeValue = CodeTextBox.Text;
                UpdateTitle();
            }
            catch (Exception x)
            {
                MessageBox.Show(x.Message, "Can't open file");
                MRU.Items.Remove(e.FileName);
            }
        }

        /// <summary>
        /// Update window title based on current file name (if any) and dirty flag.
        /// </summary>
        private void UpdateTitle()
        {
            var s = "Untitled";
            if (!string.IsNullOrEmpty(currentFileName)) s = System.IO.Path.GetFileName(currentFileName);
            if (CodeTextBox.Text != baseCodeValue) s += "*";
            this.Text = s + " - " + baseTitle;
        }

        private void newToolStripMenuItem_Click(object sender, EventArgs e)
        {
            if (CheckUnsavedChanges()) return;
            currentFileName = null;
            CodeTextBox.Text = "";
            baseCodeValue = CodeTextBox.Text;
            UpdateTitle();
        }

        private void openToolStripMenuItem_Click(object sender, EventArgs e)
        {
            if (CheckUnsavedChanges()) return;
            OpenFileDialog ofd = new OpenFileDialog();
            ofd.Filter = "Core language program file (*.core)|*.core";
            if (ofd.ShowDialog() == DialogResult.OK)
            {
                //Add the file to the MRU.Items collection using
                //the MRU.Insert method...

                MRU.Insert(ofd.FileName);
                MRU.UpdateMRUMenu(recentFilesToolStripMenuItem);

                using (var tr = new StreamReader(ofd.OpenFile()))
                {
                    CodeTextBox.Text = tr.ReadToEnd();
                    baseCodeValue = CodeTextBox.Text;
                    currentFileName = ofd.FileName;
                    UpdateTitle();
                }
            }
        }

        private void saveToolStripMenuItem_Click(object sender, EventArgs e)
        {
            doSaveOrSaveAs();
        }

        private void saveAsToolStripMenuItem_Click(object sender, EventArgs e)
        {
            doSaveAs();
        }

        private void analyzeToolStripMenuItem_Click(object sender, EventArgs e)
        {
            Analyze(false);
        }

        /// <summary>
        /// Check if there are unsaved changes, if so, prompt user to save, discard or cancel the 
        /// operation.
        /// </summary>
        /// <returns>Returns true if user elected to cancel the operation, false otherwise.</returns>
        private bool CheckUnsavedChanges()
        {
            bool cancel = false;
            if (CodeTextBox.Text != baseCodeValue)
            {
                var rc = MessageBox.Show("You have unsaved changes! Save them?", "Warning", MessageBoxButtons.YesNoCancel);
                if (rc == System.Windows.Forms.DialogResult.Yes)
                {
                    if (!doSaveOrSaveAs()) cancel = true;
                }
                else if (rc == System.Windows.Forms.DialogResult.Cancel)
                {
                    cancel = true;
                }
            }
            return cancel;
        }

        /// <summary>
        /// Save current file, assumes there is a current file.
        /// </summary>
        /// <returns>Returns true if successful, false otherwise.</returns>
        private bool doSave()
        {
            try
            {
                File.WriteAllText(currentFileName, CodeTextBox.Text);
                MRU.Insert(currentFileName);
                MRU.UpdateMRUMenu(recentFilesToolStripMenuItem);
                baseCodeValue = CodeTextBox.Text;
                UpdateTitle();
                return true;
            }
            catch (Exception x)
            {
                MessageBox.Show("Failed to save (" + x.Message + ")");
                return false;
            }
        }

        /// <summary>
        /// Prompt the user for a target file path and save the current code there.
        /// </summary>
        /// <returns>Returns true if successful, false otherwise.</returns>
        private bool doSaveAs()
        {
            SaveFileDialog ofd = new SaveFileDialog();
            ofd.Filter = "Core language program file (*.core)|*.core";
            ofd.AddExtension = true;
            if (ofd.ShowDialog() == DialogResult.OK)
            {
                currentFileName = ofd.FileName;
                return doSave();
            }
            return false;
        }

        /// <summary>
        /// Calls 'save' or 'save as' depending on what's appropriate.
        /// </summary>
        /// <returns>Return true if the save was successful, false otherwise.</returns>
        private bool doSaveOrSaveAs()
        {
            if (string.IsNullOrEmpty(currentFileName))
                return doSaveAs();
            else
                return doSave();
        }

        private void CodeTextBox_TextChanged(object sender, EventArgs e)
        {
            UpdateTitle();
        }
    }
}
